HOL Light
定理証明支援系
OCamlで書かれている。
HOLのLightバージョン...?
OCamlが動かすのに必要
HOL Light
HOL Light: an overview
GitHub: jrh13/hol-light: The HOL Light theorem prover
HOL Lightのインストール
HOL Lightとは? - ATPとCASのこと
関連
『定理証明支援系 Coq 入門 SSReflect 中心』
#定理証明支援系